Nuprl Lemma : rfunction_void_wf
2,24
postcript
pdf
{
f
|
x
:Void
Void}
Type
latex
Definitions
True
,
t
T
,
T
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
x
(
s
)
,
{
T
}
,
x
:
A
.
B
(
x
)
,
P
Q
,
Prop
Lemmas
true
wf
origin
Void} 
Type Void} Type T
T
x:A. B(x)
Q